;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Ivolatility
  (sig daily-volatility (stock))
  (sig get-all-daily-volatilities (stocks))
  (sig volatility (ticker start end tree))
  (sig volatility-query-with-tickers (tickers start end tree))
  (sig volatility-query (start end tickers tree))
  
  
  ;date needs to be string if it is used
  (con daily-volatility-returns-rational
       (implies (and (and (and (and (and (and
                                     (stringp date)
                          (stringp ticker))
                     (natp opening-price))
                     (natp highest-price))
                     (natp lowest-price))
                     (natp closing-price))
                     (natp shares-traded))
                (equal t (ratp (daily-volatility (list date ticker opening-price highest-price
                                                       lowest-price closing-price shares-traded))))))
  (con volatility-returns-string-rational-pair-tst
       (implies (and (stringp start) (stringp end) (stringp ticker))
                (equal t (and (stringp (car (volatility start end ticker tree)))
                              (rationalp (cadr (volatility start end ticker tree)))))))
  (con volatility-query-returns-string-tst
       (implies (and (stringp start) (stringp end) (string-listp tickers))
                (equal t (stringp (volatility-query start end tickers tree)))))
       )

